package subtyped


/**
 * Following typechecking as in Types and Programming Languages by Benjamin Pierce, chap 9-10-11
 *
 */

   
class TypeExc(s: String) extends Exception(s) 

object LTerm {
 
  def typeOf(t: LTerm):LType = typeOf(t,new Context[VarBinding](Nil) )
  
  def typeOf(t: LTerm, ctx: Context[VarBinding]) : LType= t match {
    case Lit(x)     => TyInt
    case Tru()      => TyBool
    case Fls()      => TyBool 
    case Unit()     => TyUnit
    case If(cond,pos,neg) => {
      if (!(TyBool equals typeOf(cond,ctx) )) throw new TypeExc("conditional not boolean")
      val typepos = typeOf(pos,ctx);val typeneg = typeOf(neg,ctx)
      val typejoin = joinOfTypes(typepos, typeneg)
      if (( typejoin equals TyTop)) throw new TypeExc("branches of if differ in type: "+typepos+" vs "+typeneg)
      typepos
    }
    case Record(fields)       => {
      val f: (String,LTerm) => (String, LType) =  (li,ti) => (li, typeOf(ti, ctx))
      val fieldtys = fields.map(Function.tupled(f))
      TyRecord(fieldtys)
    }
    case RecProj(t,index) => {
      typeOf(t,ctx) match {
        case TyRecord(fields) =>
             try {
               fields.filter( x => x._1 == index).head._2 
             }
             catch {case e: Exception => throw new TypeExc("no index "+index+" in record")
             }
        case _         => throw new TypeExc("trying to project a non record")
      }
      
    }
    case Let(Name(str),t1,t2) => {
      val typeInsert = typeOf(t1, ctx)
      val ctx2 = ctx + (str, new VarBinding(typeInsert))
      typeOf(t2, ctx2)
    }
    case V(n)       => {
      try {ctx(n).ltype}
      catch {
      case e: Exception => throw new TypeExc("unknown var: "+n)
      }
    }
    case L(x,ty,t) => {
      val ctx2 : Context[VarBinding] = ctx + (x,new VarBinding(ty))
      TyArr(ty, LTerm.typeOf(t,ctx2))
    }
    case A(t1,t2)  => {
      val ty1 = LTerm.typeOf(t1,ctx)
      val ty2 = LTerm.typeOf(t2,ctx)
      ty1 match {
        case TyArr(ty1D, ty1G) => {  
          if (subtype( ty2,ty1D) ) ty1G
          else throw new TypeExc("receive "+ (if(ty2==null) "untyped" else ty2) 
              +" but expect "+ (if(ty1D==null)"" else ty1D))
        }
        case _                 => {
          throw new TypeExc("applying to non function type")
        }
      }
    }
  }
  
  def subtype (tyS: LType, tyT: LType): boolean = {
    if (tyS == tyT) true else {
     
      (tyS,tyT) match {
      case (TyRecord(fs), TyRecord(ft)) => 
      	try {
      	ft.forall( bt=> 
         subtype( fs.filter( bs => bs._1 == bt._1).head._2, bt._2)    
              )
        } catch { case e: Exception => false}
      
      case (_,TyTop()) => true
      case (TyArr(tyS1,tyS2), TyArr(tyT1, tyT2)) =>
       (subtype(tyT1,tyS1) & subtype(tyS2,tyT2))
      case (_,_) => false
      }
    }
  }
  
  def joinOfTypes(a: LType, b: LType): LType = (a,b) match {
    case (TyTop(), _)        => TyTop
    case (_, TyTop())        => TyTop
    case (TyBool(), TyBool()) => TyBool
    case (TyInt(), TyInt())   => TyInt
    case (TyRecord(afields),TyRecord(bfields)) => {
    	val commonfields = afields.flatMap( 
                                   {case (ida,tya) => (
    	                            bfields.filter({case(idb,tyb) => ida == idb }) 
                                            . map ({case (idb,tyb) => (ida,joinOfTypes(tya, tyb))}) 
                                   ) })
  	TyRecord(commonfields)
  }
    case (TyArr(tya1,tya2),TyArr(tyb1,tyb2)) => {
      val meet = meetOfTypes(tya1, tyb1) getOrElse TyTop //{throw new TypeExc("no supertype can be found for functions" +a +" and " +b)}
      val join = joinOfTypes(tya2, tyb2)
      TyArr(meet, join)
    }

    case (_,_) => TyTop
  }
  
  
  import scala.collection.mutable.HashMap
  def meetOfTypes(a: LType, b: LType):Option[LType] = (a,b) match {
    case (TyTop() , x)         => Some(x)
    case (x       , TyTop())   => Some(x)
    case (TyBool(), TyBool())  => Some(TyBool)
    case (TyInt() , TyInt())   => Some(TyInt)
    case (TyRecord(afields), TyRecord(bfields)) => {
      var union = HashMap.empty[String,LType]
      union ++ afields
      bfields.foreach({case (i,t)=> if (!(union contains i)) union update (i,t) 
                                    else union update (i, meetOfTypes(union(i), t) getOrElse {return None})})
      Some(TyRecord(union.elements.toList))
    }
    case (TyArr(tya1,tya2), TyArr(tyb1, tyb2))  => {
      for (val tydom <- Some(joinOfTypes(tya1, tyb1));
           val tygoal <- meetOfTypes(tya2,tyb2))
           yield TyArr(tydom, tygoal)
    }
    case (_,_) => None
  }
  
  def eval(t: LTerm) : LTerm= {
    try {
    val t_bis = eval1 (t)
    eval (t_bis)
    } 
    catch { case e: NoReductionPossibleExc => t }
  }
    
    
  case class NoReductionPossibleExc extends Exception
    
  def eval1(t: LTerm): LTerm = t match {
    case If(c,p,n) if (isValue(c))            =>
         if (c equals Tru) p else n
    case If(c,p,n)                            => If(eval1(c),p,n)
    case A( L(s,ty,t12), v2) if (isValue(v2)) => termSubstTop(v2,t12)
    case A(t1, t2)                            =>
         if (isValue(t1) ) 
              A(t1 ,eval1(t2))
         else 
              A(eval1(t1), t2)
    case Let(Name(n),v1,t2) if (isValue(v1))  => termSubst(0,v1,t2)
    case Let(Name(n),t1,t2)                   => Let(Name(n),eval1(t1),t2)
    case RecProj(r@Record(fields),index) 
      if ( isValue(r))   =>
    	val matches = fields.filter( Function.tupled( (s,i) => (s == index)) )
        matches.head._2
    case RecProj(Record(fields),index)        =>
            //just map eval1 onto all nonvalues?
      def eval1first(fs:List[(String,LTerm)]) :List[(String,LTerm)]= {
        val h = fs.head
        if (isValue(h._2)) h::eval1first(fs.tail)
        else (h._1,eval1(h._2))::fs.tail
      }
      RecProj(Record(eval1first(fields)),index)
    case RecProj(t, index)                =>
      RecProj(eval1(t),index)
    case _                                    =>
         throw NoReductionPossibleExc
  }
  
  
  //types are actually irrelevant during evaluation, could use null everywhere
  def isValue(t: LTerm) : Boolean= t match {
    case L(_,_,_) => true
    case Lit(v)   => true
    case Tru()    => true
    case Fls()    => true
    case Unit()   => true
    case Record(fields) => fields.map(_ _2) forall(isValue)
    case _        => false
  }
  
  def termSubstTop(v: LTerm, t: LTerm): LTerm = {
    termShift(-1, 
              termSubst(0, 
                        termShift(1,v),
                        t ) )
  }
  def termShift(d: Int, t: LTerm) = {
  /*  def walk(c: Int,t: LTerm) :LTerm = t match {
      case V(nb)         => if (nb >= c) V(nb+d) else V(nb)
      case L(x,ty,t1)    => L(x,ty, walk(c+1, t1))
      case A(t1,t2)      => A(walk(c,t1),walk(c,t2))
      case Tru()         => Tru
      case Fls()         => Fls
      case Lit(v)        => Lit(v)
      case If(cond,p,n)  => If(walk(c,cond),walk(c,p),walk(c,n))  
    }
    walk(0,t)
  */  
    termMap((c:Int,x:V) => if (x.n >=c) V(x.n+d) else V(x.n) ,d,t)
  }
  
  def termSubst(j: Int, s: LTerm,t: LTerm) = {
  /*  def walk(c: Int, t: LTerm):LTerm = t match {
      case V(nb)         => if (nb == j+c) termShift(c,s) else V(nb)
      case L(x,ty,t1)    => L(x,ty, walk(c+1, t1))
      case A(t1,t2)      => A(walk(c,t1),walk(c,t2))
      case Tru()         => Tru
      case Fls()         => Fls
      case Lit(v)        => Lit(v)
      case If(cond,p,n)  => If(walk(c,cond),walk(c,p),walk(c,n))
    }
    walk(0,t)
  */
    termMap((c:Int,x:V) => if (x.n == j+c) termShift(c,s) else V(x.n),j,t)
  }
  def termMap(onvar:(Int,V)=>LTerm, i:Int, t:LTerm) ={
    //TODO: can you generalise this into a library for dealing with de Bruijn indices?
    // i.e., clients of that library should just write a map that calls the right function for every AST construct
    // (--> provide helper for binders and variables)
       
    def walk(c: Int, t: LTerm) : LTerm = t match {
      case V(nb)        => onvar(c,V(nb))
      case L(x,ty,t1)   => L(x,ty,walk(c+1,t1))
      case A(t1,t2)     => A(walk(c,t1),walk(c,t2))
      case Tru()         => Tru
      case Fls()         => Fls
      case Record(fields)=> {
        val fields_ = fields.map(x=> (x._1, walk(c,x._2)))
        Record(fields_)
      }
      case RecProj(r,i)  => RecProj(walk(c,r),i)
            case Unit()        => Unit
      case Lit(v)        => Lit(v)
      case If(cond,p,n)  => If(walk(c,cond),walk(c,p),walk(c,n))  
    }
    walk(0,t)
  }
   
  

}

